This research work receives symbols as input variables, simulates the execution of program, extracts the constraints binding with execution paths, such as security constraints, attack constraints and defense constraints, and constructs the SAT judgment matrix and UNSAT judgment matrix as injection vulnerabilities analysis models. According to the logical reduction results of the matrices, the states of injection vulnerabilities are decided. In the controlled experiments, the false positive and false negative ratios are greatly reduced, and the prototype system can generate correct exploits automatically.